(set-logic QF_BV)
(set-info :source |

   The benchmark encodes 2 simple processors
   receiving instructions to decode and execute.
   The processors compute the same function on 6 operands but
   their decoding units differ in the way they
   communicate the result.
   We check that, modulo reinterpretation of the
   decoded instructions, the result is the same.
   We added a "mode" flag to force the decoding
   unit to return the result in two different ways.

   The encoded design is a modification of Example 11.2, at page 20 of
   "Introduction to Verilog", by Peter M. Nyasulu
   available online.

   Generated by Roberto Bruttomesso <roberto.bruttomesso@gmail.com>

|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun opcode () (_ BitVec 8))
(declare-fun operator1 () (_ BitVec 8))
(declare-fun opr1_1 () (_ BitVec 8))
(declare-fun op1_1 () (_ BitVec 8))
(declare-fun opr1_2 () (_ BitVec 8))
(declare-fun op1_2 () (_ BitVec 8))
(declare-fun operator2 () (_ BitVec 8))
(declare-fun opr2_1 () (_ BitVec 8))
(declare-fun op2_1 () (_ BitVec 8))
(declare-fun opr2_2 () (_ BitVec 8))
(declare-fun op2_2 () (_ BitVec 8))
(declare-fun operator3 () (_ BitVec 8))
(declare-fun opr3_1 () (_ BitVec 8))
(declare-fun op3_1 () (_ BitVec 8))
(declare-fun opr3_2 () (_ BitVec 8))
(declare-fun op3_2 () (_ BitVec 8))
(declare-fun operator4 () (_ BitVec 8))
(declare-fun opr4_1 () (_ BitVec 8))
(declare-fun op4_1 () (_ BitVec 8))
(declare-fun opr4_2 () (_ BitVec 8))
(declare-fun op4_2 () (_ BitVec 8))
(declare-fun operator5 () (_ BitVec 8))
(declare-fun opr5_1 () (_ BitVec 8))
(declare-fun op5_1 () (_ BitVec 8))
(declare-fun opr5_2 () (_ BitVec 8))
(declare-fun op5_2 () (_ BitVec 8))
(declare-fun operator6 () (_ BitVec 8))
(declare-fun opr6_1 () (_ BitVec 8))
(declare-fun op6_1 () (_ BitVec 8))
(declare-fun opr6_2 () (_ BitVec 8))
(declare-fun op6_2 () (_ BitVec 8))
(declare-fun decode_1 () (_ BitVec 49))
(declare-fun dec_func_1 () (_ BitVec 1))
(declare-fun deci_func_1 () (_ BitVec 1))
(declare-fun func_1 () (_ BitVec 1))
(declare-fun out_1 () (_ BitVec 8))
(declare-fun mode_1 () (_ BitVec 1))
(declare-fun decode_2 () (_ BitVec 49))
(declare-fun dec_func_2 () (_ BitVec 1))
(declare-fun deci_func_2 () (_ BitVec 1))
(declare-fun func_2 () (_ BitVec 1))
(declare-fun out_2 () (_ BitVec 8))
(declare-fun mode_2 () (_ BitVec 1))
(assert (let ((?v_12 (= opr1_1 operator1)) (?v_13 (= opcode (_ bv136 8))) (?v_5 (= dec_func_1 (_ bv1 1))) (?v_0 (= opr2_1 operator2)) (?v_1 (= opr3_1 operator3)) (?v_2 (= opr4_1 operator4)) (?v_3 (= opr5_1 operator5)) (?v_4 (= opr6_1 operator6)) (?v_14 (= opcode (_ bv137 8))) (?v_6 (= dec_func_1 (_ bv0 1))) (?v_15 (= opcode (_ bv138 8))) (?v_7 (= opr2_1 (_ bv1 8))) (?v_8 (= opr3_1 (_ bv1 8))) (?v_9 (= opr4_1 (_ bv1 8))) (?v_10 (= opr5_1 (_ bv1 8))) (?v_11 (= opr6_1 (_ bv1 8))) (?v_16 (= deci_func_1 (_ bv1 1))) (?v_17 (= deci_func_1 (_ bv0 1))) (?v_18 (= mode_1 (_ bv0 1))) (?v_19 (= func_1 ((_ extract 48 48) decode_1))) (?v_20 ((_ extract 47 40) decode_1)) (?v_21 ((_ extract 39 32) decode_1)) (?v_22 ((_ extract 31 24) decode_1)) (?v_23 ((_ extract 23 16) decode_1)) (?v_24 ((_ extract 15 8) decode_1)) (?v_25 ((_ extract 7 0) decode_1)) (?v_38 (= opr1_2 operator1)) (?v_31 (= dec_func_2 (_ bv1 1))) (?v_26 (= opr2_2 operator2)) (?v_27 (= opr3_2 operator3)) (?v_28 (= opr4_2 operator4)) (?v_29 (= opr5_2 operator5)) (?v_30 (= opr6_2 operator6)) (?v_32 (= dec_func_2 (_ bv0 1))) (?v_33 (= opr2_2 (_ bv1 8))) (?v_34 (= opr3_2 (_ bv1 8))) (?v_35 (= opr4_2 (_ bv1 8))) (?v_36 (= opr5_2 (_ bv1 8))) (?v_37 (= opr6_2 (_ bv1 8))) (?v_39 (= deci_func_2 (_ bv1 1))) (?v_40 (= deci_func_2 (_ bv0 1))) (?v_41 (= mode_2 (_ bv0 1))) (?v_42 ((_ extract 48 41) decode_2)) (?v_43 (= func_2 ((_ extract 40 40) decode_2))) (?v_44 ((_ extract 39 32) decode_2)) (?v_45 ((_ extract 31 24) decode_2)) (?v_46 ((_ extract 23 16) decode_2)) (?v_47 ((_ extract 15 8) decode_2)) (?v_48 ((_ extract 7 0) decode_2))) (and ?v_12 (ite ?v_13 (and ?v_5 ?v_0 ?v_1 ?v_2 ?v_3 ?v_4) (ite ?v_14 (and ?v_6 ?v_0 ?v_1 ?v_2 ?v_3 ?v_4) (ite ?v_15 (and ?v_5 ?v_7 ?v_8 ?v_9 ?v_10 ?v_11) (and ?v_6 ?v_7 ?v_8 ?v_9 ?v_10 ?v_11)))) ?v_12 (ite ?v_13 (and ?v_16 ?v_0 ?v_1 ?v_2 ?v_3 ?v_4) (ite ?v_14 (and ?v_17 ?v_0 ?v_1 ?v_2 ?v_3 ?v_4) (ite ?v_15 (and ?v_16 ?v_7 ?v_8 ?v_9 ?v_10 ?v_11) (and ?v_17 ?v_7 ?v_8 ?v_9 ?v_10 ?v_11)))) (ite ?v_18 (= decode_1 (concat (concat (concat (concat (concat (concat dec_func_1 opr1_1) opr2_1) opr3_1) opr4_1) opr5_1) opr6_1)) (= decode_1 (concat (concat (concat (concat (concat (concat deci_func_1 opr6_1) opr5_1) opr4_1) opr3_1) opr2_1) opr1_1))) (ite ?v_18 (and ?v_19 (= op1_1 ?v_20) (= op2_1 ?v_21) (= op3_1 ?v_22) (= op4_1 ?v_23) (= op5_1 ?v_24) (= op6_1 ?v_25)) (and ?v_19 (= op6_1 ?v_20) (= op5_1 ?v_21) (= op4_1 ?v_22) (= op3_1 ?v_23) (= op2_1 ?v_24) (= op1_1 ?v_25))) (ite (= func_1 (_ bv1 1)) (= out_1 (bvadd (bvadd (bvadd (bvadd (bvadd op1_1 op2_1) op3_1) op4_1) op5_1) op6_1)) (= out_1 (bvor (bvor (bvor (bvor (bvor op1_1 op2_1) op3_1) op4_1) op5_1) op6_1))) ?v_38 (ite ?v_13 (and ?v_31 ?v_26 ?v_27 ?v_28 ?v_29 ?v_30) (ite ?v_14 (and ?v_32 ?v_26 ?v_27 ?v_28 ?v_29 ?v_30) (ite ?v_15 (and ?v_31 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37) (and ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37)))) ?v_38 (ite ?v_13 (and ?v_39 ?v_26 ?v_27 ?v_28 ?v_29 ?v_30) (ite ?v_14 (and ?v_40 ?v_26 ?v_27 ?v_28 ?v_29 ?v_30) (ite ?v_15 (and ?v_39 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37) (and ?v_40 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37)))) (ite ?v_41 (= decode_2 (concat (concat (concat (concat (concat (concat opr1_2 dec_func_2) opr2_2) opr3_2) opr4_2) opr5_2) opr6_2)) (= decode_2 (concat (concat (concat (concat (concat (concat opr6_2 deci_func_2) opr5_2) opr4_2) opr3_2) opr2_2) opr1_2))) (ite ?v_41 (and (= op1_2 ?v_42) ?v_43 (= op2_2 ?v_44) (= op3_2 ?v_45) (= op4_2 ?v_46) (= op5_2 ?v_47) (= op6_2 ?v_48)) (and (= op6_2 ?v_42) ?v_43 (= op5_2 ?v_44) (= op4_2 ?v_45) (= op3_2 ?v_46) (= op2_2 ?v_47) (= op1_2 ?v_48))) (ite (= func_2 (_ bv1 1)) (= out_2 (bvadd (bvadd (bvadd (bvadd (bvadd op1_2 op2_2) op3_2) op4_2) op5_2) op6_2)) (= out_2 (bvor (bvor (bvor (bvor (bvor op1_2 op2_2) op3_2) op4_2) op5_2) op6_2))) (= mode_1 mode_2) (not (= out_1 out_2)))))
(check-sat)
(exit)
